[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification ablock-store-refsize-cons
enrich
   address-list-set
, 
   ablock-nodes
with
   

   
   
   functions  . .size : address-set → nat;
              . | . : address-set × nat → address-set;
   predicates  refsize-cons : store × address-set;
               valid-adrs : address-set;
   
   
   
   

   

   axioms size-emp :  ⊦ ∅.size = 0;
          used for: s, ls;
          size-rec :  ⊦ ¬ adr ∈ as → (as ++ adr).size = as.size + adr.size;
          used for: s, ls;
          refsize-cons-def :  ⊦ refsize-cons(st, as) ↔ (∀ n. n ∈ st → st[n].ref-size = (as | n).size);
          used for: ls;
          restrict-leb :  ⊦ adr ∈ as | n ↔ adr.lnum = n ∧ adr ∈ as;
          used for: ws, lws;
          valid-adrs :  ⊦ valid-adrs(as) ↔ (∀ adr. adr ∈ as → adr.size ≠ 0);
          used for: ls;

   

   
end enrich